$\forall$$A$, $B$:Type, $x$:$A$, $y$:$B$, $a$:Atom1.
\\[0ex]AtomFree(Type;$A$) $\Rightarrow$ AtomFree(Type;$B$) $\Rightarrow$ ($\langle$$x$$,\,$$y$$\rangle$:$A$$\times$$B$$>>$$a$ $\Leftrightarrow$ $x$:$A$$>>$$a$ $\vee$ $y$:$B$$>>$$a$)